or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
↳ QTRS
↳ Overlay + Local Confluence
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))
MEM(x, union(y, z)) → MEM(x, z)
MEM(x, union(y, z)) → OR(mem(x, y), mem(x, z))
MEM(x, union(y, z)) → MEM(x, y)
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
MEM(x, union(y, z)) → MEM(x, z)
MEM(x, union(y, z)) → OR(mem(x, y), mem(x, z))
MEM(x, union(y, z)) → MEM(x, y)
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
MEM(x, union(y, z)) → MEM(x, z)
MEM(x, union(y, z)) → OR(mem(x, y), mem(x, z))
MEM(x, union(y, z)) → MEM(x, y)
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
MEM(x, union(y, z)) → MEM(x, z)
MEM(x, union(y, z)) → MEM(x, y)
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MEM(x, union(y, z)) → MEM(x, z)
MEM(x, union(y, z)) → MEM(x, y)
[MEM1, union2]
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
or(true, x0)
or(x0, true)
or(false, false)
mem(x0, nil)
mem(x0, set(x1))
mem(x0, union(x1, x2))